\begin{tabbing}
w{-}machine{-}independent($w$;$i$;$k$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it Choose}$,${\it Trans}$,${\it Send}$ = w{-}machine($w$;$i$) in \+
\\[0ex]$\forall$$s_{1}$:($x$:Id$\rightarrow\mathbb{Q}\rightarrow$w{-}vartype($w$; $i$; $x$)), $s_{2}$:($x$:Id$\rightarrow\mathbb{Q}\rightarrow$w{-}vartype($w$; $i$; $x$)).
\\[0ex]($\forall$$z$:Id. ($\neg$($z$ = $x$ $\in$ Id)) $\Rightarrow$ ($s_{1}$($z$) = $s_{2}$($z$) $\in$ $\mathbb{Q}\rightarrow$w{-}vartype($w$; $i$; $z$)))
\\[0ex]$\Rightarrow$ \=((\=$\forall$$v$:w{-}kindtype($w$.TA($i$);$w$.M;$i$)($k$).\+\+
\\[0ex](\=$\forall$$z$:Id.\+
\\[0ex]($\neg$($z$ = $x$ $\in$ Id)) $\Rightarrow$ (${\it Trans}$($k$,$v$,$s_{1}$,$z$) = ${\it Trans}$($k$,$v$,$s_{2}$,$z$) $\in$ $\mathbb{Q}\rightarrow$w{-}vartype($w$; $i$; $z$)))
\-\\[0ex]\& ${\it Send}$($k$,$v$,$\lambda$$x$.$s_{1}$($x$,0)) = ${\it Send}$($k$,$v$,$\lambda$$x$.$s_{2}$($x$,0)) $\in$ (w{-}Msg($w$) List))
\-\\[0ex]\& (\=($\uparrow$islocal($k$))\+
\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$.\+
\\[0ex]${\it Choose}$(act($k$),$n$,$\lambda$$x$.$s_{1}$($x$,0))
\\[0ex]=
\\[0ex]${\it Choose}$(act($k$),$n$,$\lambda$$x$.$s_{2}$($x$,0))
\\[0ex]$\in$ ((w{-}kindtype($w$.TA($i$);$w$.M;$i$)($k$)) + Unit))))
\-\-\-\-
\end{tabbing}